Common Knowledge Logic in a Higher Order Proof Assistant
Identifieur interne : 001620 ( Main/Exploration ); précédent : 001619; suivant : 001621Common Knowledge Logic in a Higher Order Proof Assistant
Auteurs : Pierre Lescanne [France]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: This paper presents experiments on common knowledge logic, conducted with the help of the proof assistant Coq. The main feature of common knowledge logic is the eponymous modality that says that a group of agents shares a knowledge about a certain proposition in a inductive way. This modality is specified by using a fixpoint approach. Furthermore, from these experiments, we discuss and compare the structure of theorems that can be proved in specific theories that use common knowledge logic. Those structures manifest the interplay between the theory (as implemented in the proof assistant Coq) and the metatheory.
Url:
DOI: 10.1007/978-3-642-37651-1_11
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 001580
- to stream Istex, to step Curation: 001562
- to stream Istex, to step Checkpoint: 000246
- to stream Main, to step Merge: 001632
- to stream Main, to step Curation: 001620
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Common Knowledge Logic in a Higher Order Proof Assistant</title><author><name sortKey="Lescanne, Pierre" sort="Lescanne, Pierre" uniqKey="Lescanne P" first="Pierre" last="Lescanne">Pierre Lescanne</name><affiliation><country>France</country><placeName><settlement type="city">Lyon</settlement><region type="region" nuts="2">Rhône-Alpes</region></placeName><orgName type="universitySchool" n="3">École normale supérieure de Lyon</orgName></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:5DFF9195FEDB5D2EAE42F77277725FEFD983FAC7</idno><date when="2013" year="2013">2013</date><idno type="doi">10.1007/978-3-642-37651-1_11</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-FP8RSB8P-8/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">001580</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001580</idno><idno type="wicri:Area/Istex/Curation">001562</idno><idno type="wicri:Area/Istex/Checkpoint">000246</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">000246</idno><idno type="wicri:doubleKey">0302-9743:2013:Lescanne P:common:knowledge:logic</idno><idno type="wicri:Area/Main/Merge">001632</idno><idno type="wicri:Area/Main/Curation">001620</idno><idno type="wicri:Area/Main/Exploration">001620</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Common Knowledge Logic in a Higher Order Proof Assistant</title><author><name sortKey="Lescanne, Pierre" sort="Lescanne, Pierre" uniqKey="Lescanne P" first="Pierre" last="Lescanne">Pierre Lescanne</name><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>Laboratoire de l’Informatique du Parallélisme, École Normale Supérieure de Lyon, 46, Allée d’Italie, 69364, Lyon 07</wicri:regionArea><placeName><region type="region" nuts="2">Auvergne-Rhône-Alpes</region><region type="old region" nuts="2">Rhône-Alpes</region><settlement type="city">Lyon 07</settlement></placeName><placeName><settlement type="city">Lyon</settlement><region type="region" nuts="2">Rhône-Alpes</region></placeName><orgName type="universitySchool" n="3">École normale supérieure de Lyon</orgName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country><placeName><settlement type="city">Lyon</settlement><region type="region" nuts="2">Rhône-Alpes</region></placeName><orgName type="universitySchool" n="3">École normale supérieure de Lyon</orgName></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: This paper presents experiments on common knowledge logic, conducted with the help of the proof assistant Coq. The main feature of common knowledge logic is the eponymous modality that says that a group of agents shares a knowledge about a certain proposition in a inductive way. This modality is specified by using a fixpoint approach. Furthermore, from these experiments, we discuss and compare the structure of theorems that can be proved in specific theories that use common knowledge logic. Those structures manifest the interplay between the theory (as implemented in the proof assistant Coq) and the metatheory.</div></front></TEI><affiliations><list><country><li>France</li></country><region><li>Auvergne-Rhône-Alpes</li><li>Rhône-Alpes</li></region><settlement><li>Lyon</li><li>Lyon 07</li></settlement><orgName><li>École normale supérieure de Lyon</li></orgName></list><tree><country name="France"><region name="Auvergne-Rhône-Alpes"><name sortKey="Lescanne, Pierre" sort="Lescanne, Pierre" uniqKey="Lescanne P" first="Pierre" last="Lescanne">Pierre Lescanne</name></region><name sortKey="Lescanne, Pierre" sort="Lescanne, Pierre" uniqKey="Lescanne P" first="Pierre" last="Lescanne">Pierre Lescanne</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001620 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 001620 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:5DFF9195FEDB5D2EAE42F77277725FEFD983FAC7
|texte= Common Knowledge Logic in a Higher Order Proof Assistant
}}
| This area was generated with Dilib version V0.6.33. |  |